$\forall$${\it es}$:ES, $T$, ${\it T'}$:Type, $R$:($T$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$), $P_{1}$, $P_{2}$, $Q_{1}$, $Q_{2}$:(E$\rightarrow\mathbb{P}$), $f$:(\{$e$:E$\mid$ $P_{1}$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q_{1}$($e$)\} ).
\\[0ex]($\forall$$e$:E. $P_{1}$($e$) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $Q_{1}$($e$) $\Rightarrow$ (valtype($e$) $\subseteq$r ${\it T'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $P_{1}$($e$) $\Leftarrow\!\Rightarrow$ $P_{2}$($e$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $Q_{1}$($e$) $\Leftarrow\!\Rightarrow$ $Q_{2}$($e$))
\\[0ex]$\Rightarrow$ (($e$.$P_{1}$($e$) $\rightarrow$$e$.$f$($e$)$\rightarrow$ $e$.$Q_{1}$($e$)) with $R$ $\Leftarrow\!\Rightarrow$ ($e$.$P_{2}$($e$) $\rightarrow$$e$.$f$($e$)$\rightarrow$ $e$.$Q_{2}$($e$)) with $R$)